sorted($L$) $\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$$\forall$$i$:int\_seg(0; $\parallel$$L$$\parallel$), $j$:int\_seg(0; $i$). $L$[$j$] $\leq$ $L$[$i$]